#include<iostream>
#include<fstream>
#include<vector>

using namespace std;
int main()
{
// ......................   liczba zmiennych i klauzul
 //vector <char> formula;
 int p = 100;     // liczba zmiennych
 int n = 160;     // liczba klauzul
 int k = 3;       // k SAT
 // nagłówek:p cnf 28161 139716

// ................................. wektor zmiennych
 vector <int> zmienne(p,2);        // 2 wartosc nieokreslona

//................................ wyswietlamy wektor zmiennych
 for(vector<int>::size_type i=0;i<zmienne.size();++i){
	cout << zmienne[i] << "\t";
	}


// ...................... wektor fomula wczytany z pliku  o podanej nazwie

  cout<<"Podaj nazwę pliku cnf do sprawdzenia spełnialności: ";
  char nazwa_plik[30];
  cin.get ( nazwa_plik, 30);
  cin.ignore();

  vector <vector <int> > formula(n);
  for(vector<int>::size_type i=0; i<formula.size(); ++i) {
	  formula[i].resize(k);                 //resize(3, 5);
  }
  //formula[1][1]=7;
  //cout<< "\n" << formula[1][1];
  //cout<< "\n" << formula[0][0];

  ifstream pliktxt;
  pliktxt.open(nazwa_plik);
  int liczba,i=0,j=0;
  do{
	pliktxt >> liczba;
	if(liczba == 0) ++i;
	else{
	  formula[i][j]=liczba;
	  ++j;
	  if(j%k==0) j=0;
	}

  } while(!pliktxt.eof());

  pliktxt.close();

//......... wyswietlamy wektorek
  for(vector<int>::size_type i=0;i<formula.size(); ++i) {
	  for(int j=0;j<k;++j){
	    cout << formula[i][j]<<"\t";
	   }
	   cout << endl;
  }



 //.................................... 1. eliminacja powtarzajacych sie fomul na razie dla 3-SAT
 for(vector<int>::size_type i=0;i<formula.size(); ++i) {
	 int a = formula[i][0], b=formula[i][1], c=formula[i][2];
	 for(int j=i+1;j<n;++j){
		if( formula[j][0]== a && formula[j][1]== b && formula[j][2]== c){
			formula.erase (formula.begin()+j);
			--n;
		}
	}
 }

cout <<"\n\n A po redukcji 1.\n";
  for(vector<int>::size_type i=0;i<formula.size(); ++i) {
	  for(int j=0;j<k;++j){
	    cout << formula[i][j]<<"\t";
	   }
	   cout << endl;

  }

   //.................................... 2. eliminacja klauzul zawierających p i ~p na razie dla 3-SAT
 for(vector<int>::size_type i=0;i<formula.size(); ++i) {
	 int a = formula[i][0], b=formula[i][1], c=formula[i][2];

		if( a==-b ){
			formula.erase (formula.begin()+i);
			if(a>0)
				zmienne[a]=1;
			else
				zmienne[b]=1;
			--n;
		}
		if( b == -c){
			formula.erase (formula.begin()+i);
			if(b>0)
				zmienne[a]=1;
			else
				zmienne[c]=1;
			--n;
		}
		if( a == -c){
			formula.erase (formula.begin()+i);
			if(a>0)
				zmienne[a]=1;
			else
				zmienne[c]=1;
			--n;
		}

 }

cout <<"\n\n A po redukcji 2.\n";
  for(vector<int>::size_type i=0;i<formula.size(); ++i) {
	  for(int j=0;j<k;++j){
	    cout << formula[i][j]<<"\t";
	   }
	   cout << endl;

  }

  cout <<"Liczba klauzul po redukcji: " << n << "!!!!\n\n";
  //................................ wyswietlamy wektor zmiennych
 for(vector<int>::size_type i=0;i<zmienne.size();++i){
	cout << zmienne[i] << "\t";
	}
//.............................. Koniec zabawy
 cout << "\n Koniec zabawy :-)";

  /*for(int i=0,rzut=0; i<500; i++)
  {
	   rzut = int(tekst[i]);
	   tekst[i] = char((rzut + klucz)% 256);
       cout << tekst[i];

  }
  getchar();
  cout<<"Podaj nazwę pliku do zapisu: ";
  char nazwa_plik1[30];
  cin.get ( nazwa_plik1, 30);
  cin.ignore();
  ofstream pliks;
  pliks.open(nazwa_plik1);
  pliks << tekst;
  pliks.close();*/

return 0;
}
